Verification problems arising from software programs and system level description are naturally described at higher than Boolean level of abstraction. Reasoning at higher level has several advantages over at Boolean level. Boolean solver typically does not handle high-level structural information such as arithmetic efficiently. Furthermore, the propositional encoding i.e., bit-blasting leads to large formulae depending on the data widths. Satisfiability Modulo Theory (SMT) solvers for higher-level theories such as theory of Equality and Un-interpreted Functions (EUF), Difference Logic (DLS), Bit-vector (BV) and Linear Integer Arithmetic () have shown quite promising results recently.
SMT solves the problem of deciding the satisfiability of a first-order formula with respect to a background decidable first-order equational theory T (SMT(T)). For the verification of complex designs, one often needs to solve decision problems containing integer non-linear constraints. Due to the undecidability of the problem, one usually considers bounded integers and then either linearizes the formula into a SMT() problem (i.e., theory of linear integer arithmetic with Boolean constraints) or bit-blasts into a SAT problem.
For the theory of integer non-linear operations, the decision problem is un-decidable. Therefore, the decision procedures for such a theory typically assume bounded integer operands. Such an assumption is generally justified, given the verification problems arising from various hardware/software domains use finite width integer (words). Such non-linear operations do arise often, though used sparingly, in system design and verification. Traditionally, integer non-linear operations are handled in Boolean logic by bit-blasting all operands. However, there are some inherent disadvantages in reasoning at the Boolean level. Propositional translations of richer data types such as integers, and high-level expressions such as arithmetic, lead to large bit-blasted formulas. Moreover, the high-level semantics such as arithmetic are often “lost” in such low-level translation, thereby, the SAT search becomes more difficult.
With the growing use of high-level design abstraction to capture today's complex design features, the focus of verification techniques has been shifting from propositional reasoning towards SMT solvers, and SMT-based verification methods such as bounded model checking (BMC). To capitalize on these workhorses, encoding for integer non-linear operations such as multiplication can be carried out using linearization, i.e., one of the operands of multiplication is bit-blasted, and the result is expressed as linear arithmetic operations.
Linearization for non-linear datapaths has been studied in the context of Register Transfer Level (RTL) verification. RTL is a high-level hardware description language (HDL) for defining digital circuits. In RTL verification, linear arithmetic constraints are generated for linear and non-linear datapaths, and are encoded into integer linear programming (ILP) expressions. In, a special attention was given to the modulo semantics. In, a linearization encoding with Booleanization (bit-extraction) was used to generate SMT() i.e., theory of Linear Integer Arithmetic with Boolean constraints. In these approaches, integer bounds were added eagerly as bounding constraints. To handle modulo semantics, additional constraints were also added eagerly.
As reconfirmed in our experiments, the integer bounding constraints cause the solver to slow down significantly, especially, when added eagerly. To overcome this, approaches have used abstraction/refinement of bounds in decision procedure for solving bit-vector and Presburger theories. Other approaches have used un-interpreted functions for abstracting datapaths, accompanied with iterative refinement steps. These approaches are based on bit-blasted encoding, and therefore, they make it difficult to refine the formula without re-encoding it. Re-encoding in Boolean domain typically “destroys” the learning done by DPLL-style SAT solvers and thereby affects the performance of the solvers, as the learning need to be rediscovered. Moreover, it is not obvious how to guide SAT solvers using high-level constraints, as SAT solvers are usually “oblivious” of arithmetic expressions.
The theory of bit-vector SMT(BV) is inherently non-linear. In practice, SMT(BV) solvers use SMT() in the last stage after linearizing bit-vector operations or use complete bit-blasting after applying re-write and inference rules at the preprocess/online stage. In, a decision procedure for non-linear congruences (i.e., equalities on bounded integers) is presented, however, it does not address non-linear inequalities.
Computer algebra systems such as Maxima are intended for the manipulation of symbolic and numerical expressions including factorization, and solving linear equations. However, such systems can not be directly applied to software verification methods such as SMT-based BMC.